Termination Proof Script

• Consider the SCC {24}. There are no usable rules. By taking the AF π with π(ADD) = 1 together with the lexicographic path order with empty precedence, rule 24 is strictly decreasing.


• Consider the SCC {23}. There are no usable rules. By taking the AF π with π(DBL) = 1 together with the lexicographic path order with empty precedence, rule 23 is strictly decreasing.


• Consider the SCC {26}. There are no usable rules. By taking the AF π with π(HALF) = 1 together with the lexicographic path order with empty precedence, rule 26 is strictly decreasing.


• Consider the SCC {21}. There are no usable rules. By taking the AF π with π(SQR) = 1 together with the lexicographic path order with empty precedence, rule 21 is strictly decreasing.


• Consider the SCC {25,28}. There are no usable rules. By taking the AF π with π(ACTIVATE) = 1, π(FIRST) = π(n__first) = 2 and π(cons) = [2] together with the lexicographic path order with empty precedence, rule 28 is weakly decreasing and rule 25 is strictly decreasing.